COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	notes[w85,jmc]		Notes and ideas
C00008 ENDMK
C⊗;
notes[w85,jmc]		Notes and ideas

1985 Jan 14

Here are some problems on which I'm stuck.

1. How to extend the blocks world formalism, so as to get a less
trivial domain.  Ideas include towers, creating and destroying
blocks.

2. There is also the problem of proving that a tower structure
re-arranging program works.  We need a way of saying that there
are a finite number of finite towers.  Circumscription is fine
for showing that an enumerated towere is finite, but how do we
say that a tower is finite without specifying how many elements
it has.

3. We are looking for a new decidable case of the decision problem
that will cover AI examples.  The intuition is that the number
of kinds of elements in an AI problem is finite.  Idea: perhaps
this isn't even true for relationship formulas.

Suppose we have the functions  father(x), mother(x) and the predicates
male(x) and female(x).  We have just the axioms
∀x.male(father(x)) and  ∀x.female(mother(x)).  It looks like all
the other relationships are definable, e.g.

∀x.brother(x,y) ≡ male(y) ∧ father(x)=father(y) ∧ mother(x) = mother(y).

Query: Is the set of all true formulas in father,mother, male, female
decidable?
If not, we should look for a decidable subset in accordance with the
idea that what we humans think about such relationships cannot
be deep.

4. Consider the 8 queens problem as one of putting queens on the
board until one either finds a solution or gets stuck and backtracks
in some way.  Our basic formalism should not be committed to place
queens by rows.  It can also maintain other data structures such
as lists of excluded squares.  Excluded squares can be marked on
the board itself, and this works fine, but in general one should
allow extra data structures.  The following problems arise.
a. The symmetries of the board generate symmetries of placements.
The program should be advisable about fact regarding symmetries
and should then take them into account.  It isn't proper for the
human to do the work of writing a search that takes the symmetries
into account before the computer even sees the problem.
b. Since we aren't committed to go by rows, we have to do something
to avoid searching parts of the space over.  What?
c. We want the program to be modifiable by advice that excludes
a placing a queen so as to kill a row or, more generally, require
an unfillable configuration.
d. Can we use the pigeonhole principle for more than the corner
+ knights move configuration.

(item c) involves theorems like

dead(r,c) ; row r is dead in configuration c.

add(x,c) ; the configuration that results from putting a queen on x
in configuration c.

kill(x,c) ; the configuration that results from excluding square x
in configuration c.

illegal(c); two queens attack each other in c

dead(r,add(x,c)) ⊃ excludable(x,c)

It looks, therefore, like a configuration should specify excluded
squares as well.

extends(c1,c2); configuration c2 extends c1 in the sense that it
has more or the same queens and more or the same excluded squares.

inev(c1,c2); configuration c2 extends c1 in the strong sense that
any solution starting with c1 extends c2.

excludable(x,c) ⊃ inev(c,kill(x,c))